\begin{tabbing}
$\forall$\=${\it es}$:ES, $A$:Type, ${\it ds}$:$x$:Id fp$\rightarrow$ Type,\+
\\[0ex]${\it conds\_list}$:($k$:Knd fp$\rightarrow$ $V$:Type $\times$ (State(${\it ds}$)$\rightarrow$$V$$\rightarrow$($A$ + Top)) List), $i$:Id.
\-\\[0ex]($\forall$${\it conds}$$\in$${\it conds\_list}$. es{-}triggers{-}params{-}consistent(${\it es}$;$A$;$i$;${\it ds}$;${\it conds}$))
\\[0ex]$\Rightarrow$ ($\forall$${\it conds}_{1}$,${\it conds}_{2}$$\in$${\it conds\_list}$.  ${\it conds}_{1}$ $\parallel$ ${\it conds}_{2}$)
\\[0ex]$\Rightarrow$ (\=p{-}first(map($\lambda$${\it conds}$.es{-}triggers(${\it es}$;$i$;${\it ds}$;${\it conds}$);${\it conds\_list}$))\+
\\[0ex]=
\\[0ex]es{-}triggers(${\it es}$;$i$;${\it ds}$;$\oplus$(${\it conds\_list}$))
\\[0ex]$\in$ AbsInterface($A$))
\-
\end{tabbing}